p:. (p) = p 

latex

Up	bool 1, bool 1
Definitions	t  T, x:A. B(x), tt, ff, if b then t else f fi , b, Unit, ,
Lemmas	bool wf, btrue wf, bfalse wf